Terrence Tao - Lean

Terry Tao posted on Mastodon that he found a bug in a proof in one of his papers thanks to trying to formalize it in Lean. This is an excellent use case of Lean and tbh the only one that I think is going to be taken seriously for a while.